package model.cnf;

import java.io.File;
import java.io.IOException;
import java.util.List;

/**
 * Represent a CNF.
 * 
 * @author GRONOWSKI Stephane svan001@aol.com
 * 
 *         igsat 2010
 * 
 */
public abstract class CNF {
	public static final String	PREFIX				= "";
	public static final String	SUFFIX				= ".export.cnf";

	// aide a la lecture de CNF dans un fichier
	public static final char	COMMENTAIRE			= 'c';
	public static final char	DESCRIPTION			= 'p';
	public static final int		SIZE_DESCRIPTION	= 5;

	protected File				CNFfile;
	protected int				declaredNumVar;
	protected int				declaredNumClause;
	protected boolean			modify				= false;

	protected Stat				stat				= null;

	/**
	 * 
	 * @return the declared number of variable.
	 */
	public int getDeclaredNumVar() {
		return declaredNumVar;
	}

	/**
	 * 
	 * @return the declared num of clause.
	 */
	public int getDeclaredNumClause() {
		return declaredNumClause;
	}

	/**
	 * 
	 * @return if the CNF has been modify.
	 */
	public boolean isModify() {
		return modify;
	}

	/**
	 * Set if the CNF has been modify.
	 * 
	 * @param modify
	 */
	public void setModify(boolean modify) {
		this.modify = modify;
	}

	/**
	 * 
	 * @return the name of the file associate with the CNF.
	 */
	public String getFileName() {
		return CNFfile.getName();
	}

	/**
	 * 
	 * @return the {@link Stat} associate to the CNF.
	 */
	public Stat getStat() {
		return stat;
	}

	/**
	 * Change the Stat of the CNF.
	 * 
	 * @param stat
	 *            new stat.
	 */
	public void setStat(Stat stat) {
		this.stat = stat;
	}

	/**
	 * Ask to check the {@link Stat} of the CNF.
	 * 
	 * @throws IOException
	 *             if there is a problem
	 */
	public abstract void checkStat() throws IOException;

	/**
	 * 
	 * @return the {@link File} associate to the CNF.
	 */
	public File getCNFfile() {
		return CNFfile;
	}

	/**
	 * 
	 * @return the size of the CNF, means number of clause.
	 */
	public int size() {
		return declaredNumClause;
	}

	/*
	 * public int getNumVar() throws IOException { return declaredNumVar; }
	 */

	/**
	 * Export the CNF a in File format.
	 * 
	 * @param cnf
	 *            pathname of the file.
	 * @param directory
	 *            the directory to save the CNF.
	 * @return the file.
	 */
	public abstract File export(String cnf, File directory);

	/**
	 * Export the CNF in File format.
	 * 
	 * @param directory
	 *            the directory to save the CNF.
	 * @return the file.
	 */
	public abstract File export(File directory);

	/**
	 * Return all the clause of the CNF.
	 * 
	 * @return all the clause of the CNF.
	 * @throws Exception.
	 */
	public abstract List<Clause> getClauses() throws IOException;

	/**
	 * Check the CNF for modification.
	 * 
	 * @throws Exception.
	 */
	public abstract void check() throws IOException;

	/**
	 * Add a list of clause to the CNF.
	 * 
	 * @param cl
	 *            the list clause to add.
	 */
	public abstract void addClause(List<Literal> cl);

	/**
	 * Add a clause to the CNF.
	 * 
	 * @param cl
	 *            the clause to add.
	 */
	public abstract void addClause(Clause cl);

	/**
	 * Get the clause number "i" in the CNF.
	 * 
	 * @param i
	 *            the number of the clause.
	 * @return the clause number "i".
	 * @throws IOException
	 *             if something goes wrong with the file.
	 * @throws IllegalArgumentException
	 *             if the clause "i" doen't exist.
	 */
	public abstract Clause getClause(int i) throws IllegalArgumentException, IOException;

	/**
	 * Close the cnf, mean close all the open file if there are and export if change has been made.
	 * 
	 * @return if everything was fine.
	 */
	public abstract boolean close();

	/**
	 * close the cnf, mean close all the open file if there are without exporting the cnf.
	 */
	public abstract void closeWithoutExport();
}
